es-secret-server{$table:ut2, $encrypt:ut2, $decrypt:ut2}
es-secret-server(es; T; L; i)
== let ds = "$table" : secret-table(T) in
== let ds(discrete(i;"$table"))
== let & (lL.
== let & (destination(l) = i
== let & (& state ds
== let & (& rcv(l,"$encrypt")::( + Atom1)  data(T) sends ["$encrypt", e.next("$table" when e)::
== let & (&  Atom1] on lnk-inv(l)
== let & (& state ds
== let & (& rcv(l,"$decrypt")::( + Atom1)
== let & (&  Atom1 sends ["$decrypt", e.decrypt("$table" when e;val(e)):data(T)] on lnk-inv(l))
== let & (@i only map(l.rcv(l,"$encrypt");L) affect "$table":secret-table(T)
== let & (c ((lL.
== let & (c ((@i 
== let & (c ((@i events of kind rcv(l,"$encrypt") change "$table" to
== let & (c ((@i es,v. encrypt(s."$table";v) State(ds) (val::( + Atom1)  data(T)))
== let & (c & e@i.
== let & (c & e':E
== let & (c & (e leaks "$table" to e'
== let & (c &  (lL.(kind(e) = rcv(l,"$encrypt") & kind(e') = rcv(lnk-inv(l),"$encrypt"))
== let & (c &   (kind(e) = rcv(l,"$decrypt") & kind(e') = rcv(lnk-inv(l),"$decrypt"))))
== let & (c & e@i. e copies "$table"
== let & (c & e@i.
== let & (c & (first(e))
== let & (c &  (atoms-distinct("$table" when e)
== let & (c &  & ptr("$table" when e) = 0
== let & (c &  & (n:, j:Id.
== let & (c &  & ((n < ||"$table" when e|| )  j || st-atom("$table" when e;n)  (j = i))))) 

latex

---

clarification:

es-secret-server{$table:ut2, $encrypt:ut2, $decrypt:ut2}
es-secret-server(es; T; L; i)
== let ds = "$table" : secret-table(T) in
== let ds(es-isconst(es;i;"$table"))
== let & l_all(L;IdLnk;l.destination(l) = i  Id
== let & es-kind-sends-iff(es;rcv(l,"$encrypt");:( + Atom1)  data(T);lnk-inv(l);"$encrypt";:
== let  Atom1;ds;e.next(es-when(es; "$table"; e)))
== let & es-kind-sends-iff(es;rcv(l,"$decrypt");:( + Atom1)
== let &  Atom1;lnk-inv(l);"$decrypt";data(T);ds;e.decrypt(es-when(es; "$table"; e);es-val
== let & (es; e))))
== let & (es-frame(es;i;map(l.rcv(l,"$encrypt");L);"$table";secret-table(T))
== let & (c (l_all(L;IdLnk;l.effect-p(es;i;ds;rcv(l,"$encrypt");:( + Atom1)
== let & (c  data(T);"$table";s,v. encrypt(s."$table";v)))
== let & (c & alle-at(es;i;e.e':es-E(es)
== let & (c & alle-at(es;i;e.(es-leaks(es;e;"$table";e')
== let & (c & alle-at(es;i;e. l_exists(L;IdLnk;l.(es-kind(es; e) = rcv(l,"$encrypt")  Knd
== let & (c & alle-at(es;i;e. & es-kind(es; e') = rcv(lnk-inv(l),"$encrypt")  Knd)
== let & (c & alle-at(es;i;e.  (es-kind(es; e) = rcv(l,"$decrypt")  Knd
== let & (c & alle-at(es;i;e.  & es-kind(es; e') = rcv(lnk-inv(l),"$decrypt")  Knd))))
== let & (c & alle-at(es;i;e.es-copies(es;e;"$table"))
== let & (c & alle-at(es;i;e.(es-first(es; e))
== let & (c &  (atoms-distinct(es-when(es; "$table"; e))
== let & (c &  & ptr(es-when(es; "$table"; e)) = 0  
== let & (c &  & (n:, j:Id.
== let & (c &  & ((n < ||es-when(es; "$table"; e)|| )
== let & (c &  & ( es-atom(es;j;st-atom(es-when(es; "$table"; e);n))
== let & (c &  & ( (j = i  Id)))))) 

latex

Definitions

let x = a in b(x), x : v, discrete(i;x), destination(l), next(tab), state dsk:A sends [tg, e.f(e):B] on l, decrypt(tab;kval), val(e), A c B, @i only L affect x:T, map(f;as), secret-table(T), xL. P(x), @i events of kind k change x to f State(ds) (val:T), x:A  B(x), left + right, Atom$n, data(T), x.A(x), encrypt(tab;keyv), s.x, x:A. B(x), E, e leaks x to e', (xL.P(x)), IdLnk, P  Q, Knd, kind(e), rcv(l,tg), lnk-inv(l), A, e copies x, e@i. P(e), b, first(e), atoms-distinct(tab), P & Q, ptr(tab), #$n, , x:A. B(x), a < b, ||tab|| , P  Q, i || a, st-atom(tab;n), x when e, "$x", s = t, Id